\begin{tabbing}
$\forall$$x$, ${\it tg}$:Id, $k$:Knd, $l$:IdLnk, $T$, $A$, $B$:Type.
\\[0ex](rcv($l$,${\it tg}$) $=$ $k$ $\Rightarrow$ $T$ $=$ $B$)
\\[0ex]$\Rightarrow$ (\=$\forall$$f$:($A$$\rightarrow$$B$$\rightarrow$$T$), $c$:($A$$\rightarrow$$B$$\rightarrow\mathbb{B}$).\+
\\[0ex]@source($l$): $k$(v) sends [${\it tg}$,   $\lambda$$a$,$b$. if $c$($a$,$b$)$\rightarrow$ [$f$($a$,$b$)] else nil fi($x$, v)] on link $l$  
\\[0ex]$\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@source($l$): $k$(v) sends [${\it tg}$,   $\lambda$$a$,$b$.
\\[0ex]if $c$($a$,$b$)$\rightarrow$ [$f$($a$,$b$)] else nil fi($x$, v)] on link $l$  
\\[0ex]$\subseteq$
\\[0ex]$D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]vartype(source($l$);$x$) $\subseteq\rho$ $A$
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ source($l$) $\in$ Id $\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $B$)
\\[0ex]\& ($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ \=(\=$c$(($x$ when $e$),val($e$))\+\+
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]\& \=sender(${\it e'}$) $=$ $e$ $\in$ E\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex]kind(${\it e''}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ sender(${\it e''}$) $=$ $e$ $\in$ E
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\in$ E)
\-\\[0ex]\& val(${\it e'}$) $=$ $f$(($x$ when $e$),val($e$)) $\in$ $T$))
\-\-\-\\[0ex]\& (\=$\neg$$c$(($x$ when $e$),val($e$))\+
\\[0ex]$\Rightarrow$ $\neg$($\exists$${\it e'}$:E. kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd \& sender(${\it e'}$) $=$ $e$ $\in$ E)))))
\-\-\-\-\-\-
\end{tabbing}